\section{Synchronous syntax}

$$
\begin{array}{lrlr}
u & ::=  &   x, y  \sepr a, b & \text{names}	\\
 k & ::=  &   x, y \sepr \cha^{+}, \cha^{-} & \text{channels}	\\
d & ::= & a, b  \,\sepr \cha^{+}, \cha^{-} & \text{identifiers} \\
v & ::= & \mathtt{true}, \mathtt{false} \sepr a, b  \sepr \cha^{+}, \cha^{-} & \text{values} \\
e & ::= & v \sepr x, y, z  \sepr d = d & \text{expressions} \\
%  & \sepr & \arrive{u}  \sepr \arrive{k} \sepr \arrive{k,h} & \text{arrive predicates (usual)}\\ 
  & \sepr & \arrive{\locf{loc}, r} & \text{arrive predicate for locations}\\ 
P & ::=  &   \nopenr{u}{x:\ST}.P  & \text{session request}	\\
	& \sepr &   \nopena{u}{x:\ST}.P  & \text{session acceptance}	\\
	& \sepr &  \outC{k}{e}.P & \text{data output}\\
  	&\sepr &    \inC{k}{x}.P  & \text{data input}\\
	&\sepr&   \select{k}{n};P & \text{selection}\\
    &\sepr&   \branch{k}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m} & \text{branching}\\
    &\sepr&   \mu \rv{X}.P & \text{recursion} \\
	& \sepr &   \rv{X}& \text{recursion variable} \\
  	& \sepr &  \ifte{e}{P}{Q} & \text{conditional}\\
  	& \sepr &   P \para  P & \text{parallel composition}\\	 
		&\sepr&   \close{k}.P & \text{close session}	\\
	&\sepr&   \restr{\cha}{P}  & \text{channel hiding}	\\
	&\sepr&   \restr{a}{P}  & \text{name hiding}	\\
	&\sepr&   \mathbf{0}  & \text{inaction} \\
	&\sepr&   \que{\cha}{\ST}  & \text{session queue} \\ 
	
	&\sepr&  \scomponent{\locf{loc}}{P}  & \text{located process }\\
%	&\sepr&  \nadapt{l}{P} & \text{update process}\\
	&\sepr&  \nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m_i}^{}{:}\STT_{m_i}^{i}}}{Q_i}{i \in I}} \quad& \text{typeful update process }\\
	&\sepr&   \outC{\locf{loc}}{r}  & \text{adaptation signal} \\
	&\sepr&   \que{\locf{loc}}{\til{r}}  & \text{queue for locations} \\
%p	&::= &  + \sepr - &\text{channel polarities} \\
h	&::= &  v \sepr n &\text{messages}  \\
r	&::= &  \mathtt{upd}_I \sepr \mathtt{upd}_E \sepr\mathtt{upg} \sepr \cdots &\text{adaptation messages} 
%    & \sepr &   e_1 + e_2 \sepr e_1 - e_2  \sepr \mathtt{not}(e) \sepr  \ldots & \text{expressions}
\end{array} 
$$






\section{Synchronous semantics}

AGGIUNGERE UNA REGOLA DI CONGRUENZA SULLE CODE


$$
\begin{array}{ll}
 \rulename{r:Par} & \text{if } P \pired P' ~~\text{then} ~~ P \para Q \pired P' \para Q  \vspace{2mm}
\\
\rulename{Eval} & \text{if }e \pired e' \text{ then } \evc{E}[e] \pired \evc{E}[e']
\vspace{2mm}\\
\rulename{Cont} &  \text{if }P \pired P' \text{ then } \locc{P} \pired \locc{P'}
\vspace{2mm}\\
\rulename{NRes} & \text{if }P \pired P' \text{ then } (\nu a)P \pired (\nu a)P'
\vspace{2mm}\\
\rulename{CRes} &\text{if }P \pired P' \text{ then } (\nu \cha)P \pired (\nu \cha)P'
\vspace{2mm}\\
 \rulename{r:Str} &
\text{if } P \equiv P',\, P' \pired Q', \,\text{and}\, Q' \equiv Q ~\text{then} ~ P \pired Q \vspace{2mm}
\\
  \rulename{r:Loc} &
 \text{if } P \pired P'~~\text{then}~~ \scomponent{l}{P} \pired \scomponent{l}{P'} \vspace{2mm}
 \\ 
 \rulename{r:Open} & 
C\{\nopena{u}{x:\ST}.P\} \para  D\{\nopenr{u}{y:\overline{\ST}}.Q\} \pired  \\
& 
\hfill \restr{\cha}{\big({C\{P\sub{\cha^+}{x} \para \que{\cha^p}{\ST} \}  \para  D\{Q\sub{\cha^-}{y} \para \que{\cha^{\overline{p}}}{\overline{\ST}}     \}\big) } \vspace{2.0mm} \\

\rulename{r:COMM} &
C\{\outC{\cha^{\,p}}{v}.P \para \que{\cha^p}{!(T).\ST} \} \para  D\{\inC{\cha^{\,\overline{p}}}{{x}}.Q \para  \que{\cha^{\overline{p}}}{?(T).\overline{\ST}}}\} 
\pired \\
&\hfill
C\{P \para \que{\cha^p}{\ST} \} \para  D\{Q\sub{{c}\,}{{x}} \para \que{\cha^{\overline{p}}}{\overline{\ST}} \} \quad ({e} \downarrow {c}) \vspace{2mm}
\\
\rulename{r:Sel} &
C\{\branch{\cha^{\,p}}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m} \para  \que{\cha^p}{\&\{n_j{:}\ST_j\}_{j \in J}} \} \para \\
& D\{\select{\cha^{\,\overline{p}}}{n_j};Q \para \que{\cha^{\overline{p}}}{\oplus\{n_j:\overline{\ST_j} \}_{j \in J}}  \} 
\pired \\
& 
\hfill C\{P_j \para \que{\cha^p}{\ST_j} \}\para  D\{Q \para \que{\cha^{\overline{p}}}{\overline{\ST_j}} \}  \quad (1 \leq j \leq m)  \vspace{2mm}
\\
\rulename{r:Close} &
C\{\close{\cha^{\,p}}.P \para \que{\cha^p}{\varepsilon} \} \para  D\{\close{\cha^{\,\overline{p}}}.Q \para \que{\cha^{\overline{p}}}{\varepsilon}\} \pired %\\
%& \hfill 
C\{P\} \para  D\{Q\} \vspace{ 2mm}
\\
\rulename{r:IfTr} &
\ifte{\mathtt{true}}{P}{Q} \pired P    \vspace{2mm}
\\
 \rulename{r:IfFa} &
\ifte{\mathtt{false}}{P}{Q} \pired Q   \vspace{2mm}\\
\rulename{UpdReq} &  \locc{\que{\locf{loc}}{\til{r}_1}} \para \locd{\outC{\locf{loc}}{r}} \pired 
\locc{\que{\locf{loc}}{\til{r}_1 \cdot r}} \para \locd{D[\mathbf{0}}
\vspace{2mm}\\
\rulename{Arrive} & \locc{\evc{E}[\arrive{\locf{loc},r}]} \para \locd{\que{\locf{loc}}{\til{r}}} \pired \locc{\evc{E}[\mathtt{b}]}
\para \locd{\que{\locf{loc}}{\til{r}}}  \quad ((|\til{r}| \geq 1) \downarrow \mathtt{b}) 
\vspace{4mm}\\
\rulename{UpdateD} & 
\displaystyle\frac{
\begin{array}{rcr} 
\mathsf{fc}(P) = \til{\cha} = \cha_1^p, \ldots, \cha^p_n 
& &
R = \que{\cha^p_1}{\ST_1} \para \cdots \para \que{\cha^p_n}{\ST_n} \\
 (V = P \land R' = R) & \bigvee  &
\exists \til{x}_0 \subseteq \til{x}, \rho .\big(
|\til{k}| = |\til{x}_0| \land \til{x}_0 = \{x_1, \ldots, x_g\} ~\land ~
\\ 
& & \rho = \subst{\til{\cha}\,}{\,\til{x}_0} ~\land~ I' = \{u \in I \,|\, \mathsf{fc}(Q_u) = \til{x}_0\}~\land\\
& & \exists l \in I'.(\forall j \in [1..n].\forall s \in [1..g].~~ \STT^{l}_s \leq \ST_j ~\land~ \\
&& \qquad 
\forall r < l.\exists j \in [1..n].\exists s \in [1..g].~~\STT^{r}_s \not\leq \ST_j ~\land~
\\
&&  \quad V = \rho(Q_l) ~\land~
R' = \que{\cha^p_1}{\STT_{1}^l} \para \cdots \para \que{\cha^p_n}{\STT^{l}_g} 
)  \big)
\end{array}
}{
\locc{\scomponent{\locf{loc}}{P} \para R} \para
\locd{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m_i}^{}{:}\STT_{m_i}^{i}}}{Q_i}{i \in I}}}   
\pired 
\locc{\scomponent{\locf{loc}}{V} \para R'} \para \locd{\mathbf{0}}
} 

\end{array}
$$






Our type system builds upon the ones in~\cite{DBLP:journals/entcs/YoshidaV07,Kouzapas12},
extending it so as to account for disciplined runtime adaptation.


\subsection{Type Syntax}

We now define our type syntax, which is rather standard.

 
\begin{definition}[Types]\label{d:types}
The syntax of 
 \emph{basic types} (ranged over $\capab, \sigma,   \ldots$) 
and 
 \emph{session types} (ranged over $\ST, \beta, \ldots$)
is given in Table~\ref{tab:types}.
\end{definition}

\begin{table}[t!]
\textsc{Types}
$$
\begin{array}{lclr}
T&::=& \capab, \alpha \\
\capab, \sigma & ::= & \mathsf{name} \sepr \mathsf{bool}  ~~~& \text{basic types}\\

\alpha, \beta &::=  &  !(\capab).\alpha \sepr ?(\capab).\alpha & \text{send, receive} \\ 
		& \sepr &  !(\beta).\alpha \sepr ?(\beta).\alpha & \text{throw, catch} \\ 
		& \sepr &  \&\{n_1:\alpha_1, \dots,  n_m:\ST_m \}  \quad &  \text{branch} \\
		& \sepr &  \oplus\{n_1:\alpha_1, \dots , n_m:\ST_m \}  &  \text{select} \vspace{0.5mm} \\
		& \sepr &  \epsilon \!\!\!\!\!\!& \text{closed session} \\
    & \sepr  & t & \text{type variable} \\ 
   	      & \sepr &  \mu t.\alpha & \text{recursive type} 
\end{array}
$$
\textsc{Environments}
$$
\begin{array}{lclr}
		\qua & ::= &  \qual \sepr \quau  & \text{type qualifiers} \vspace{0.5mm} \\
\ActS & ::= &  \emptyset \sepr \ActS , k:\ST \sepr \ActS ,  k:\que{}{\ST}  & \text{typing with active sessions}\\
\Gamma &::= &  \emptyset \sepr \Gamma, e:\capab \sepr \Gamma, a:\langle \ST_\qua , \overline{\ST}_\qua \rangle \quad& \text{first-order environment}\\
\Theta &::= &  \emptyset \sepr  \Theta,\mathsf{X}:\INT \sepr \Theta,l:\INT     \quad& \text{higher-order environment}
\end{array}
$$  
\caption{Types and Typing Environments. Interfaces $\INT$ are formally introduced in Definition~\ref{d:interf}.}\label{tab:types}
\end{table}


We recall the intuitive meaning of session types. 
We write $\til{\tau}$ to denote a sequence of base types $\tau_1, \ldots, \tau_n$.
Type $?(\til{\capab}).\ST$ (resp. $?(\beta).\ST$) abstracts the behavior of a channel 
which receives values of types $\til{\capab}$ (resp. a channel of type $\beta$) 
and continues as $\ST$ afterwards.
Complementarily, type $!(\til{\capab}).\ST$ (resp. $!(\beta).\ST$) represents the behavior
of a channel which sends values (resp. a channel)  and that continues as $\ST$ afterwards.
Type $\&\{n_1:\alpha_1, \dots,  n_m:\ST_m \}$ describes a branching behavior, or external choice, along a channel:
it offers $m$ behaviors, and if the $j$-th alternative is selected then it behaves as described by type $\ST_j$ ($1 \leq j \leq m$).
In turn, type $\oplus\{n_1:\alpha_1, \dots , n_m:\ST_m \}$ describes the behavior of a channel which 
may select a single behavior among  $\alpha_1, \ldots, \alpha_m$. This is an internal choice, which continues as $\ST_j$ afterwards.
Finally, type $\epsilon$ represents a channel with no communication behavior. 
We now introduce the subtyping relation.


\begin{definition}
A relation $\mathcal{R} \subseteq \mathcal{T} \times \mathcal{T}$ is a \emph{type simulation}
if $(\ty, \tyy) \in \mathcal{R}$ implies the following conditions:
\begin{enumerate}[1.]
\item If $\unf{\ty} = \capab$ then $\unf{\tyy} = \sigma$ and $\capab \bsub \sigma$.

\item If $\unf{\ty} = \epsilon$ then $\unf{\tyy} = \epsilon$.

\item If $\unf{\ty} = ?(\ty_2).\ty_1$ then $\unf{\tyy} = ?(\tyy_2).\tyy_1$ and $(\ty_1, \tyy_1) \in \mcc{R}$ \\ and  $(\ty_2, \tyy_2)  \in \mcc{R}$.

\item If $\unf{\ty} = \,!(\ty_2).\ty_1$ then $\unf{\tyy} = \,!(\tyy_2).\tyy_1$ and $(\ty_1, \tyy_1) \in \mcc{R}$ \\ and  $(\tyy_2, \ty_2)  \in \mcc{R}$.

\item If $\unf{\ty} = ?(\tau_1, \ldots, \tau_n).\ty_1$ then $\unf{\tyy} = ?(\sigma_1, \ldots, \sigma_n).\tyy_1$ then
for all $i \in [1..n]$, we have that $(\tau_i, \sigma_i) \in \mcc{R}$ and $(\ty_1, \tyy_1) \in \mcc{R}$.

\item If $\unf{\ty} = !(\tau_1, \ldots, \tau_n).\ty_1$ then $\unf{\tyy} = !(\sigma_1, \ldots, \sigma_n).\tyy_1$ then
for all $i \in [1..n]$, we have that $(\sigma_i, \tau_i) \in \mcc{R}$ and $(\ty_1, \tyy_1) \in \mcc{R}$.

\item If $\unf{\ty} = \&\{n_1:\ty_1, \dots,  n_m:\ty_m \}$ then $\unf{\tyy} = \&\{n_1:\tyy_1, \dots,  n_h:\tyy_h \}$ 
and $m \leq h$
for all $i \in [1..m]$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.

\item If $\unf{\ty} = \oplus\{n_1:\ty_1, \dots,  n_m:\ty_m \}$ then $\unf{\tyy} = \oplus\{n_1:\tyy_1, \dots,  n_h:\tyy_h \}$ 
and $h \leq m$
for all $i \in [1..m]$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.

\end{enumerate}
\end{definition}

Observe how  $\subt$ is co-variant for input prefixes and contra-variant for outputs, 
whereas it is co-variant for branching and contra-variant for choices.
We have the following definition:


\begin{definition}
The coinductive subtyping relation, denoted \csub, is defined by $T \csub S$ if and only if there exists a type simulation $\mcc{R}$
such that $(T, S) \in \mcc{R}$.
\end{definition}



We now move on to define duality.


\begin{definition}
A relation $\mathcal{R} \subseteq \mathcal{T} \times \mathcal{T}$ is a \emph{duality relation}
if $(\ty, \tyy) \in \mathcal{R}$ implies the following conditions:
\begin{enumerate}[1.]
\item If $\unf{\ty} = \capab$ then $\unf{\tyy} = \sigma$ and $\tau \csub \sigma$ and  $\sigma \csub  \tau$.

\item If $\unf{\ty} = \epsilon$ then $\unf{\tyy} = \epsilon$.

\item If $\unf{\ty} = ?(\ty_2).\ty_1$ then $\unf{\tyy} = !(\tyy_2).\tyy_1$ and $(\ty_1, \tyy_1) \in \mcc{R}$ \\ and  $\ty_2 \csub \tyy_2$ and $\tyy_2 \csub \ty_2$.

\item If $\unf{\ty} = \,!(\ty_2).\ty_1$ then $\unf{\tyy} = \,?(\tyy_2).\tyy_1$ and $(\ty_1, \tyy_1) \in \mcc{R}$ \\ and  $\ty_2 \csub \tyy_2$ and $\tyy_2 \csub \ty_2$.

\item If $\unf{\ty} = ?(\tau_1, \ldots, \tau_n).\ty_1$ then $\unf{\tyy} = ?(\sigma_1, \ldots, \sigma_n).\tyy_1$ then
for all $i \in [1..n]$, we have that $(\ty_1, \tyy_1) \in \mcc{R}$ and  $\tau_i \csub \sigma_i$ and  $\sigma_i \csub  \tau_i$.

\item If $\unf{\ty} = !(\tau_1, \ldots, \tau_n).\ty_1$ then $\unf{\tyy} = ?(\sigma_1, \ldots, \sigma_n).\tyy_1$ then
for all $i \in [1..n]$, we have that $(\ty_1, \tyy_1) \in \mcc{R}$ and  $\tau_i \csub \sigma_i$ and  $\sigma_i \csub  \tau_i$.

\item If $\unf{\ty} = \&\{n_1:\ty_1, \dots,  n_m:\ty_m \}$ then $\unf{\tyy} = \oplus\{n_1:\tyy_1, \dots,  n_m:\tyy_m \}$ and
for all $i \in [1..m]$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.

\item If $\unf{\ty} = \oplus\{n_1:\ty_1, \dots,  n_m:\ty_m \}$ then $\unf{\tyy} = \&\{n_1:\tyy_1, \dots,  n_m:\tyy_m \}$ and
for all $i \in [1..m]$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.

\end{enumerate}

\end{definition}

We may now define:

\begin{definition}
The coinductive duality relation, denoted \cdual, is defined by $T \cdual S$ if and only if there exists a duality relation $\mcc{R}$
such that $(T, S) \in \mcc{R}$. The extension of $\csub$ to typings and interfaces, written $\ActS \csub \ActS'$ and $\INT \csub \INT'$, respectively, 
arise as expected.
\end{definition}


Our typing judgments generalize usual notions with an  \emph{interface}~$\INT$ (see Def.~\ref{d:interf}). 
Based on the syntactic occurrences of prefixes $\nopenr{a}{x}$, $\nopena{a}{x}$, and $\repopen{a}{x}$,
the interface of a process describes the (possibly persistent) services appearing in it.
Thus, intuitively, the interface of a process gives an ``upper bound'' on the services that a process may execute.
Formally, we have:

\begin{definition}[Interfaces]\label{d:interf}
We define an \emph{interface} as the multiset whose underlying set of elements 
$\mathrm{Int}$ contains 
assignments from names to session types which are qualified (cf. Table~\ref{tab:types}).
More precisely: $$\mathrm{Int} = \{ \qua\,a{:}\ST ~|~ \qua \in \{\qual, \quau\}, 
\text{$a$ is a name, and $\ST$ is a session type}\}$$
We use $\INT, \INT', \ldots$ to range over interfaces.
We sometimes write $\#_\INT(a) = h$ to mean that element $a$ occurs $h$ times in $\INT$.
\end{definition}

Observe how several occurrences of the same service declaration are captured by the multiset nature of interfaces.
The union of two interfaces $\INT_1$ and $\INT_2$ is essentially the union of their underlying multisets.
We sometimes write $\INT \addelta a:\ST_\qual$ 
and  $\INT \addelta a:\ST_\quau$
to stand 
for $\INT \addelta\{\qual\,a{:}\ST\}$ and 
$\INT \addelta \{\quau\,a{:}\ST\}$, respectively.

\begin{newnotation}[Interfaces]\label{n:interf}
We write $\INT_\qual$ (resp. $\INT_\quau$) to denote the subset of $\INT$ involving
only assignments qualified with $\qual$ (resp. $\quau$). 
Moreover, we write $\INT \unres$ to denote the ``persistent promotion'' of $\INT$. Formally, 
$\INT \unres = \INT \setminus \INT_\qual \addelta \{\quau\,a{:}\ST \mid   \qual\,a{:}\ST \in \INT_\qual \}$.
\end{newnotation}

It is useful to relate different interfaces. 
This is the intention of the relation $\intpr$ over interfaces, defined next.

\begin{definition}[Interface Ordering] \label{d:intpre}Given interfaces $\INT$ and $\INT'$, we write 
$\INT  \intpr \INT'$ iff 
\begin{enumerate}[1.]
\item 
One of the following holds:
\begin{enumerate}[(a)]
\item $\INT_\qual \subseteq \INT'_\qual$, where $\subseteq$ is the usual ordering on multisets, or 
\item $\forall (\qual\,a{:}\ST) \in \INT_\qual \setminus \INT_\qual'$ then  $(\quau\,a{:}\ST) \in \INT'_\quau$
\end{enumerate}
\item $\forall (\quau\,a{:}\ST) \in \INT_\quau $  then $ (\quau \, a{:}\ST) \in \INT'_\quau $.
\end{enumerate}
Interface equality is defined as: $\INT_1 = \INT_2$ iff  $\INT_1 \intpr \INT_2$ and $\INT_2 \intpr \INT_1$
\end{definition}


\subsection{Environments, Judgments and Typing Rules}
The typing environments we rely on are defined in the lower part of Table~\ref{tab:types}.
In addition to interfaces $\INT$, we consider typings $\ActS$ and environments $\Gamma$ and $\Theta$.


Typing $\ActS$ is commonly used to collect
assignments from channels to session types; as such, it describes
currently active sessions. 
In our discipline, 
in $\ActS$ we also include \emph{bracketed assignments}, denoted $[\kappa^p:\ST]$,
which represent active but restricted sessions. 
As we discuss below, bracketed assignments arise in the typing of %channel 
restriction, 
and are key to keep a precise count of the active sessions in a given located process. 
We write $dom(\ActS)$ to denote the set $\{ k^p \mid k^p:\ST \in \ActS \lor [k^p:\ST] \in \ActS\}$.
We write $\ActS , k:\ST $ and $\ActS , [k:\ST] $ where $k \not\in dom(\ActS)$.


$\Gamma$ is a first-order environment which maps expressions to basic types
and names to pairs of \emph{qualified} session types.
In  the interface, a session type is qualified with 
`$\quau$' if it is associated to a persistent service; otherwise, it is qualified with 
`$\qual$'.

The higher-order environment $\Theta$ 
collects assignments of process variables and locations to interfaces. 
While the former kind of assignments is relevant to update processes, the latter concern located processes.
As we explain next, by relying on the combination of these two pieces of information the type system ensures that
runtime adaptation actions preserve the behavioral interfaces of a process.
We write $vdom(\Theta)= \{ \mathsf{X} \mid \mathsf{X}:\INT \in \Theta \}$ to denote the variables in the domain of $\Theta$.
Given these environments, a \emph{type judgment} is  of form
$$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} $$ 
meaning that, under environments $\Gamma$ and $\Theta$, 
process $P$ has active sessions declared in $\ActS$ and interface 
$\INT$.

\begin{table}[th!]
$$
\begin{array}{c}
% \mathrm{\textsc{Comp}}~~~\component{a}{P} \arro{~\component{a}{P}~}  \star
\infer[\rulename{t:bool}]
{\typing{\Gamma}{\true, \false}{\bool}}{} 
\qquad
\infer[\rulename{t:name}]
{\typing{\Gamma}{a}{\name}}{} 
\\ \\
\infer[\rulename{t:bVar}]
{\typing{\Gamma, x: \bool }{x}{\bool}}{} 
\qquad
\infer[\rulename{t:nVar}]
{\typing{\Gamma, x: \name}{x}{\name}}{} 
\\ \\
\infer[\rulename{t:eq}]
{\typing{\Gamma}{d=d}{\bool}}{} \qquad 
\infer[\rulename{t:Ser}]
{\typing{\Gamma, a:\langle\ST, \overline{\ST}\rangle}{a}{\langle\ST, \overline{\ST}\rangle}}{} 
\\ \\



\inferrule*[right=\rulename{t:Nil}]{ }{\judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}}
\vspace{2mm} \\
\inferrule*[right=\rulename{t:LocEnv}]{ }{\typing{\Theta, \locf{loc}:\INT}{\locf{loc}}{\INT}} 
\vspace{2mm} \\
\inferrule*[right=\rulename{t:Accept}]
{\typing{\Gamma}{a}{\langle \ST_\qual , \overline{\ST}_\qual  \rangle} \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\ST}{\,\INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\nopena{u}{x:\ST}.P}{ \type{\ActS}{\,\INT \addelta u: \ST_\qual}}}
\vspace{2mm} \\
\inferrule*[right=\rulename{t:Request}]
 {\typing{\Gamma}{a}{\langle \ST_\qua , \overline{\ST}_\qual \rangle} \qquad
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\ST }{\,\INT}} 
}{\judgebis{\env{\Gamma}{\Theta}}{ \nopenr{u}{x:\ST}.P}{ \type{\ActS}{\,\INT \addelta u: {\ST}_\qual }}} 
\vspace{2mm} \\
\inferrule*[right=\rulename{t:Clo}]
 {\judgebis{\env{\Gamma}{\Theta}}{ P}{\type{\ActS}{\INT}} \qquad k\notin \dom{\ActS} }{\judgebis{\env{\Gamma}{\Theta}}{ \close{k}.P}{ \type{\ActS, k:\epsilon}{ \INT}}}
\vspace{2mm} \\

\inferrule*[right=\rulename{t:Par}]
 {
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{ \INT_1}} \qquad
 \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
 }{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{\type{\ActS_1 \cup \ActS_2}{\INT_1 \addelta \INT_2}}}

\end{array}
$$


$$
\begin{array}{c}


\infer[\rulename{t:msg}]
{\typing{\Gamma}{r_1}{\msg}}{} \qquad

\infer[\rulename{t:locQ}]
{\typing{\Gamma}{r_1;\til{r}}{\msg}}
{\typing{\Gamma}{\til{r}}{\msg} & \typing{\Gamma}{r_1}{\msg}}\\ \\

\infer[\rulename{t:arrive}]
{\judgebis{\env{\Gamma}{\Theta}}{\arrive{\locf{loc}, r}}{\bool}}
{\typing{\Theta}{\locf{loc}}{\INT} \qquad\typing{\Gamma}{r}{\msg}} \\ \\


\inferrule*[right=\rulename{t:Loc} ]
 {
       \typing{\Theta}{\locf{loc}}{\INT} \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT' } }  \qquad \INT' \intpr \INT
 }{\judgebis{\env{\Gamma}{\Theta}}{\component{\locf{loc}}{}{\INT}{P} }{ \type{\ActS}{\INT' }}}
\vspace{2mm} \\

\infer[\rulename{t:Sig}]
{\judgebis{\env{\Gamma}{\Theta}}{\outC{\locf{loc}}{r}}{\type{\emptyset}{\emptyset}}}
{\typing{\Gamma}{r}{\msg}} \qquad

\infer[\rulename{t:QLoc}]
{\judgebis{\env{\Gamma}{\Theta}}{\que{\locf{loc}}{\til{r}}}{\type{\emptyset}{\emptyset}}}
{ \typing{\Gamma}{\til{r}}{\msg}} \\ \\


\infer[\rulename{t:Adapt}]
{\judgebis{\env{\Gamma}{\Theta}}{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{j}; \cdots ;x_{m_j}^{}{:}\STT_{m_j}^{j}}}{Q_j}{j \in J}}}{\type{\emptyset}{\emptyset}}}
{\typing{\Theta}{\locf{loc}}{\INT} & \forall j \in J, \ 
\judgebis{\env{\Gamma}{\Theta}}{Q_i}{\type{x_{1}^{}{:}\STT_{1}^{j}; \cdots ;x_{m_j}^{}{:}\STT_{m_j}^{j}}{\INT_j} } \quad \INT_j \intpr \INT}

\end{array}
 $$
\caption{Well-typed processes (I)} \label{tab:ts}
\end{table}



\begin{table}[th!]
$$
\begin{array}{c}
\infer[\rulename{t:Q}]
 {\judgebis{\env{\Gamma}{\Theta}}{\que{\cha}{\ST}}{\type{\cha:\que{}{\ST}}{\emptyset}}}{}
 
\\ \\
\inferrule*[right=\rulename{t:Thr}] 
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\STT}{ \INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\outC{k}{k'}.P}{\type{\ActS, k:!(\ST).\STT, k':\ST}{ \INT}}}
\vspace{2mm} \\
\inferrule*[right=\rulename{t:Cat}]
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\STT, x:\ST}{\INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\inC{k}{x}.P }{\type{\ActS, k:?(\ST).\STT}{ \INT}}}
\vspace{2mm} \\
\inferrule*[right=\rulename{t:In}]
{\judgebis{\env{\Gamma, {x}:{\capab}}{\Theta}}{P}{\type{\ActS, k:\ST}{\INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\inC{k}{{x}}.P }{\type{\ActS, k:?({\capab}).\ST}{ \INT}}}
\vspace{2mm} \\
\inferrule*[right=\rulename{t:Out}]
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\ST}{ \INT}} \quad \typing{\Gamma}{e}{\capab}}
{\judgebis{\env{\Gamma}{\Theta}}{\outC{k}{{e}}.P}{\type{\ActS, k:!({\capab}).\ST}{ \INT}}}
\vspace{2mm} \\
\inferrule*[right=\rulename{t:Weakc}] 
{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS}{ \INT}  } \qquad \cha^+, \cha^- \notin dom(\ActS)}{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS}{ \INT }}}
\vspace{2mm} \\
\inferrule*[right=\rulename{t:Weakn}] 
{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS}{ \INT}  } \qquad a \notin dom(\INT)}
{\judgebis{\env{\Gamma}{\Theta}} {\restr{a}{P}}{\type{\ActS}{ \INT }}}
\vspace{2mm} \\
\inferrule*[right=\rulename{t:If}]
 {
 \typing{\env{\Gamma}{\Theta}}{ e}{\mathsf{bool}} \qquad
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} \qquad
\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\ActS}{\INT}}
 }{\judgebis{\env{\Gamma}{\Theta}}{\ifte{e}{P}{Q}}{\type{\ActS}{\INT}}} 
\vspace{2mm} \\
\inferrule*[right=\rulename{t:Bra}] 
{
\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS, k:\ST_1}{ \INT_1}} 
\quad 
\cdots
\quad
\judgebis{\env{\Gamma}{\Theta}}{P_m}{\type{\ActS, k:\ST_m}{ \INT_m}} \quad \INT = \INT_1 \uplus ...\uplus \INT_m
 }{\judgebis{\env{\Gamma}{\Theta}}{\branch{k}{n_1{:}P_1 \alte \cdots \alte  n_m{:}P_m}}{\type{ \ActS, k:\&\{n_1{:}\ST_1, \ldots, n_m{:}\ST_m \}}{\INT}}}
\vspace{2mm} \\
\inferrule*[right=\rulename{t:Sel}]
{
\judgebis{ \env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\ST_i}{ \INT}} \qquad 1 \leq i \leq m 
}{\judgebis{\env{\Gamma}{\Theta}}{\select{k}{n_i};P}{\type{\ActS, k:\oplus\{n_1:\ST_1, \ldots,  n_m:\ST_m \}}{\INT}}}
\end{array}
$$% \vspace{-4mm}
\caption{Well-typed processes (II)}\label{tab:session}
\end{table}

RIFLETTERE: NELLA REGOLA CRES I KAPPA FRA QUADRE NON SERVONO PIU' 

\begin{table}[t!]
$$
\begin{array}{c}
\infer[\rulename{t:RVar}]{\Gamma; \Theta,\rv X: \ActS, \INT \vdash \rv X:\type{\ActS}{\INT}}{}
\\ \\
\infer[\rulename{t:Rec} ]{\judgebis{\env{\Gamma}{\Theta}}{\mu \rv X. P}{\type{\Delta}{\INT }}} 
{\judgebis{\env{\Gamma}{\Theta,\rv X: \type{\ActS}{\INT}}}{P}{\type{\Delta}{ \INT}} }
\\ \\
\infer[\rulename{t:Subs} ]{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS'}{\INT'}} } 
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Delta}{ \INT}}& \ActS \csub \ActS' & \INT \csub \INT'}
\\
 \\
 \infer[\rulename{t:CRes}]{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS}{ \INT}}}
 {\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS, \cha^-:\ST_1, \cha^-:\que{}{\ST_1}, \cha^+:\ST_2, \cha^+:\que{}{\ST_2} }{ \INT}} & \ST_1 \cdual \ST_2} \\ \\
 
 \infer[\rulename{t:NRes}]{\judgebis{\env{\Gamma}{\Theta}} {\restr{a}{P}}{\type{\ActS}{ \INT}}}
 {\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS }{ \INT \cup \INT_a}} \ a \notin \dom{\INT} }\\
 \text{ where } \INT_a \text{ contains only declarations for } a \ (i.e. \forall b\neq a, b\notin \dom{\INT_a} )
 
\end{array}
$$
\caption{Well-typed processes with recursion and subtyping: New and/or modified rules } \label{tab:subt}
\end{table}

\begin{theorem}[Subject Reduction]\label{th:subred}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ with $\ActS$ balanced and $P \pired Q$ then 
 $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS}{\INT'}}$, for some $\INT'$.
\end{theorem}
